Polynomial Datalog Rewritings for Expressive Description Logics with Closed Predicates

1 Introduction

In ontology-mediated queries (OMQs), a database query is enriched with an ontology, providing domain knowledge to obtain more complete answers from incomplete data. OMQs are receiving much attention in the database and knowledge representation research communities, particularly when the ontological knowledge is expressed in Description Logics (DLs) or in rule-based formalisms like existential rules and DATALOG◦, see e.g., [Bienvenu et al., 2014; Bienvenu and Ortiz, 2015; Gottlob et al., 2015] and their references.

The open-world semantics of these formalisms makes them suitable for handling incomplete knowledge, but viewing all data as incomplete can result in too few certain answers. For this reason, closed predicates have been advocated as a powerful tool to combine complete and incomplete knowledge, by explicitly specifying predicates assumed complete, thus given a closed-world semantics [Franconi et al., 2011; Lutz et al., 2013]. For example, take the following ontology T (formally, a DL TBox):

Student v 9attends▷Course

BScStud v Student

BScStud v 8attends▷≻GradCourse

and the following set of facts A (an ABox):

Then (a↪ c1) is not a certain answer to the instance query q = attends(x↪ y) mediated by T , but if c1 and c2 are known to be the only courses, then (a↪ c1) should become a certain answer. This can be achieved by declaring Course a closed predicate.

In this paper, we investigate the relative expressiveness of OMQs in terms of more traditional query languages like DATALOG. More precisely, we are interested in the following problem: given an OMQ Q (specified by a query and a TBox, possibly with closed predicates), obtain a DATALOG query Q0-in a suitable fragment-such that, for any ABox A, the certain answers to Q and Q0 coincide.

The existence of such a Q0 and its size are crucial for understanding the expressive power and succinctness of different families of OMQs. However, they are also very relevant in practice, since they allow to reuse existing database technologies to support OMQ answering. For example, the research into OMQs that can be rewritten into first-order (FO) queries has produced the successful DL-Lite family [Calvanese et al., 2007]. The succinctness of FO-rewritings for DL-Lite, and for families of existential rules that are FO-rewritable, has been extensively studied [Gottlob et al., 2014a; Gottlob and Schwentick, 2012], and for cases where (succinct) FO-rewritings do not exists, some authors have considered rewritings that, unlike the ones we consider here, are not dataindependent [Kontchakov et al., 2011; Gottlob et al., 2014b].

In the presence of closed predicates, the only rewritability results are FO-rewritability for the core fragment of DL-Lite [Lutz et al., 2015], and a rewriting algorithm for queries that satisfy some strong definability criteria [Seylan et al., 2009]. Other works on OMQs with closed predicate have focused on the complexity of their evaluation, e.g., [Ngo et al., 2015; Lutz et al., 2013; Franconi et al., 2011]. The latter two have shown coNP-hardness in data complexity for many lightweight DLs, barring the existence of FO-rewritings.

Many DLs are not FO-rewritable, but can be rewritten into monotonic DATALOG queries, leading to implemented systems, e.g., [P´erez-Urbina et al., 2010; Eiter et al., 2012b; Trivela et al., 2015]. The pioneering work in [Hustadt et al., 2007] showed that instance queries in an expressive extension of ALC can be rewritten into a program in disjunctive DATALOG, using a constant number of variables per rule, but exponentially many rules. The first translation from conjunctive queries (CQs) in expressive DLs without closed predicates (SH, SHQ) to programs in disjunctive DATALOG was introduced in [Eiter et al., 2012a], but the programmay contain double exponentially many predicates. For ALC and for union of CQs, the existence of exponential rewritings into disjunctive DATALOG was shown recently [Bienvenu et al., 2014], and for restricted fragments of SHI and classes of CQs translations to DATALOG were investigated in [Kaminski et al., 2014a; 2014b]. A polynomial time DATALOG translation of instance queries was proposed in [Ortiz et al., 2010], but for a so-called Horn-DL that lacks disjunction. To our knowledge, this was until now the only polynomial rewriting for a DL that is not FO-rewritable.

In this paper, we consider the class Q of OMQs of the form (T ↪ ⌃↪ q), where q is an instance query and T is a TBox in the very expressive DL ALCHIO with closed predicates ⌃. We observe that such queries are non-monotonic. Indeed, if we take ⌃ = ¶Course♦ as the set of closed predicates in the above example, then (a↪ c1) is a certain answer to (T ↪⌃↪ q) over A, but it is not a certain answer over the extended set of facts A0 = A[ ¶Course(c3)♦. For this reason, these queries cannot be rewritten into monotonic variants of DATALOG, like positive DATALOG (with or without disjunction). The main contribution of this paper is a polynomial time translation of queries in Q into disjunctive DATALOG extended with negation as failure. Our translation is modular: if no closed predicates are present-in the case of classical instance queries in ALCHIO-our translation yields a positive disjunctive DATALOG program of polynomial size. A simplified version of this translation for ALCHI can be found in [Ahmetaj et al., 2016]. To our knowledge, this is the first polynomial time translation of an expressive (non-Horn) DL into disjunctive DATALOG.

2 Preliminaries

We give some basic notions of DLs and DATALOG.

The DL ALCHIO We assume countably infinite, mutually disjoint sets NR of role names, NC of concept names, and NI of individual names. A role r is either a role name p, or an expression p-, called the inverse of p. We let r- = p if r = p-. Concepts are defined inductively as follows:

• (i) >, ? and all A 2 NC are concepts;
• (ii) if o 2 NI, then ¶o♦ is a concept;
• (iii) if C1↪C2 are concepts, then C1 uC2, C1 tC2 and ≻C1 are concepts;
• (iv) if r is a role, and C is a concept, then 9r▷C, 8r▷C are concepts.

A concept inclusion is an expression of form C1 vC2, where C1↪ C2 are concepts. A role inclusion is an expression of form r1 v r2, where r1↪ r2 are roles. A TBox T is a finite set of (concept and role) inclusions. An ABox A is a finite set of assertions of the forms A(a) (called concept assertion) and p(a↪ b) (called role assertion), where ¶a↪ b♦ ✓ NI, A 2 NC, and p 2 NR. A knowledge base (KB) (with closed predicates) is a triple K = (T ↪ ⌃↪ A), where T is a TBox, ⌃ ✓ NC [ NR is the set of closed predicates in K, and A is an ABox.

An interpretation is a pair I = h∆I ↪ ·I i where ∆I is a non-empty set (called the domain), AI ✓ ∆I for each A 2

NC, rI ✓ ∆I ⇥ ∆I for each r 2 NR, and aI 2 ∆I for each a 2 NI. The function ·I is extended to the remaining concepts and roles in the standard way [Baader et al., 2007].

An interpretation I satisfies an inclusion q1 v q2, if qI 1 ✓ qI 2 , in symbols I ♣= q1 v q2; and it satisfies an assertion q(~a) if: (~a)I 2 qI , in symbols, I ♣= q(~a). For Γ a TBox or ABox, we write I ♣= Γ if I ♣= ↵ for all ↵ 2 Γ. For an ABox A and ⌃ ✓ NC [ NR, we write I ♣=⌃ A if

For a KB K = (T ↪⌃↪A), we write I ♣= K if the following hold: 1 (i) a 2 ∆I and aI = a for each a 2 NI occurring in K, (ii) I ♣= T , and (iii) I ♣=⌃ A. For an assertion ↵, we write K ♣= ↵ if I ♣= ↵ for all I such that I ♣= K.

Normal Form We let N+C = NC[¶¶a♦ ♣ a 2 NI♦[¶>↪?♦ be the basic concepts. Our results apply to arbitrary TBoxes, but to simplify presentation, we consider TBoxes in normal form where inclusions take one of the following forms:

Instance Queries In this paper we consider an (ontology mediated) instance query. Each such query is given as a triple Q = (T ↪⌃↪ q), where T is a TBox, ⌃ ✓ NC [ NR, and q 2 NC [ NR. Let ~a 2 NI in case q 2 NC, and ~a 2 N2I otherwise. Then ~a is a certain answer to Q over an ABox A if (T ↪⌃↪A) ♣= q(~a); note that if ⌃ = ;, this boils down to the usual DL instance checking problem. To ease presentation, we assume that every concept and role of A also occurs in T .

with r↪ s roles, ¶B1↪ ▷ ▷ ▷ ↪ Bk♦ ✓ N+C , and ¶A↪ A0 ♦ ✓ NC. We also assume that T is closed under role inclusions as follows:

• (a) p v p 2 T , for each p 2 NR occurring in T ,

For Γ a TBox, ABox, or KB, we denote by NI(Γ), NR(Γ), NC(Γ), and N+C (Γ) the set of individuals, role names, concept names, and basic concepts that occur in Γ, resp. We write r(-) 2 ⌃ to mean r 2 ⌃ if r 2 NR, and r- 2 ⌃ otherwise.

Nonmonotonic DATALOG We assume countably infinite sets NP and NV of predicate symbols (each with an associated arity) and variables, respectively. We further assume that NC [ NR ✓ NP with each A 2 NC being unary, and each r 2 NR being binary. An atom is an expression of the form R(t1↪ ▷ ▷ ▷ ↪ tn), where ¶t1↪ ▷ ▷ ▷ ↪ tn♦ ✓ NI [ NV, and R is an n-ary relation symbol. A negated atom is an expression of the form not ↵, where ↵ is an atom. A rule ⇢ is an expression of the form h1 _ ▷ ▷ ▷ _ hn b1↪ ▷ ▷ ▷ ↪ bk, where H = ¶h1↪ ▷ ▷ ▷ ↪ hn♦ is a set of atoms, called the head of ⇢, and B = ¶b1↪ ▷ ▷ ▷ ↪ bk♦ is a set of possibly negated atoms, called the body of ⇢. Each variable that occurs in the head of ⇢ must also occur in a (non-negated) atom in the body of ⇢. Rules of the form h (known as facts) are simply identified with the atom h, thus ABox assertions are valid facts in our syntax. For a role name p, we may use p-(t1↪ t2) to denote the atom p(t2↪ t1). A program is any finite set P of rules. We use ground(P ) to denote the grounding of P , i.e. the variable-free program that is obtained from P by applying on its rules all the possible substitutions of variables by individuals of P. If negated atoms do not occur in P, then P is positive.

1 We make the standard name assumption (SNA), which is common for closed predicates, for the individuals occurring in K.

An (Herbrand) interpretation (or, database) I is any finite set of variable-free (or, ground) atoms. We assume a binary built-in inequality predicate 6= with a natural meaning: in any interpretation I, a 6= b 2 I iff (i) a 6= b, and (ii) a (resp. b) occurs in an atom R(~t) 2 I, where R is not 6=. An interpretation I is a model of a positive program P if ¶b1↪ ▷ ▷ ▷ ↪ bk♦ ✓ I implies I \ ¶h1↪ ▷ ▷ ▷ ↪ hn♦ 6= ; for all rules h1 _ ▷ ▷ ▷ _ hn b1↪ ▷ ▷ ▷ ↪ bk in ground(P). We say an interpretation I is a minimal model of a positive program P if I is a model of P , and there is no J 6✓ I that is a model of P .

The GL-reduct of a program P w.r.t. an interpretation I is the program P I that is obtained from ground(P) in two steps: (i) deleting every rule that has not ↵ in the body with ↵ 2 I, and (ii) deleting all negated atoms in the remaining rules [Gelfond and Lifschitz, 1988]. An interpretation I is a stable model (also known as answer sets) of a program P if I is a minimal model of P I .

A query is a pair (P↪ q), where P is a program, and q is a predicate symbol from P. A tuple ~a of constants is a certain answer to (P↪ q) over a database I if q(~a) 2 J for all stable models J of P [ I.

3 Characterization of Counter Models

Assume a KB K = (T ↪⌃↪A) and an assertion q. Towards deciding K 6♣= q using a polynomially sized program, we decompose the problem into two steps:

1. Guess a core interpretation Ic for K, whose domain is NI(K). Core interpretations fix how the individuals of K participate in concepts and roles, ensuring the satisfaction of A and ⌃, and the non-entailment of q.
2. Check that Ic can be extended to satisfy all axioms in T .

Defining rules that do (1) is not hard, but (2) is more challenging, and will rely on a game-theoretic characterization we describe below. But first we need to define the notion of core interpretations.

Definition 1. A core interpretation for a KB K = (T ↪ ⌃↪A) is any interpretation Ic such that

• (c1) ∆Ic = NI(K) and aIc = a for all a 2 NI(K),
• (c2) Ic ♣=⌃ A,
• (c3) Ic ♣= Av8r▷A0 for all Av8r▷A0 2 T ,
• (c4) Ic ♣= r v s for all r v s 2 T ,

• (c5) Ic ♣= Av 9r▷A0 for all Av 9r▷A0 2 T , if r v s 2 T for some s(-) 2 ⌃.

An interpretation J is called an extension of Ic, if Ic is the result of restricting J to NI(K), and qJ = qIc for all q 2 ⌃.

A core and its extensions coincide on the assertions they entail, and deciding non-entailment of an instance query amounts to deciding whether there is a core that does not entail it, and that can be extended into a model. But verifying whether a core can be extended into a full model is hard, as it corresponds to testing consistency (of Ic viewed as an ABox) with respect to T , an EXPTIME-hard problem already for fragments of ALCHOI. In order to obtain a polynomial set of rules that solves this EXPTIME-hard problem, we characterize it as a game, revealing a simple algorithm that admits an elegant implementation in nonmonotonic disjunctive DATALOG. For this we use types, which we define as follows:

Definition 2. A type (over a TBox T ) ⌧ is a subset of N+C (T ) [ ¶>♦ such that ? 62 ⌧ and > 2 ⌧ . We say that ⌧ satisfies an inclusion ↵ = B1u· · ·uBnvBn+1t· · ·tBk of type (N1), if ¶B1↪ ▷ ▷ ▷ ↪Bn♦ ✓ ⌧ implies ¶Bn+1↪ ▷ ▷ ▷ ↪Bk♦ \ ⌧ 6= ;; otherwise ⌧ violates ↵. For an element e 2 ∆I in an interpretation I, we let type(e↪ I) = ¶B 2 N+C ♣ e 2 BI ♦. A type ⌧ is realized in I if there is some e 2 ∆I s.t. type(e↪ I) = ⌧.

We now describe a game to decide whether a given core Ic can be extended into a model of a KB K. The game is played by Bob (the builder), who wants to extend Ic into a model, and Sam (the spoiler), who wants to spoil all Bob's attempts. Sam starts by picking an individual a, and they look at its type type(a↪ Ic). If it doesn't satisfy certain local consistency conditions (e.g., the inclusions (N1)) Sam wins. Otherwise, in each turn Sam chooses an inclusion of the form Av 9r▷A0 which would need to be satisfied by (an element with) the current type, forcing Bob to pick a type for the corresponding r-successor that satisfies A0 . The game continues for as long as Bob can respond to the challenges of Sam.

Formally, for a TBox T , a set ⌃ ✓ NC [ NR and an interpretation I, we define the locally consistent set LC(T ↪⌃↪ I) as the set of types ⌧ over T such that:

(LCN1) ⌧ satisfies all inclusions of type (N1) in T .

(LC⌃) ⌧ must be realized in I if one of the following holds:

• (ii) A 2 ⌧ , A v 9r▷A0 2 T , r v s 2 T and s(-) 2 ⌃.
• (i) ⌧ \⌃6= ;, or

The game on I starts by Sam choosing an individual a 2 ∆I , and ⌧ = type(a↪ I) is set to be the current type. Then:

• (G) If ⌧ 62 LC(T ↪⌃↪ I), then Sam is declared winner.

Otherwise, Sam chooses an inclusion Av 9r▷A0 2 T with A 2 ⌧; if there is no such inclusion, Bob wins the game. Otherwise, Bob chooses a new type ⌧ 0 such that:

• (C1) A0 2 ⌧ 0 , and

⌧ 0 is set to be the current type, and the game continues with a new round, i.e. we go back to G.

A run of the game on I is a (possibly infinite) sequence

where a is the individual picked initially by Sam, and each ↵i and ⌧i are the inclusions picked by Sam and the type picked by Bob in round i, respectively. A strategy for Bob is a partial function str that maps pairs of a type ⌧ and an inclusion Av 9r▷A0 with A 2 ⌧ to a type ⌧ 0 that satisfies (C1) and (C2); intuitively, it gives a move for Bob in response to moves of Sam. A run a↵1⌧1↵2⌧2 ▷ ▷ ▷ with type(a↪ I) = ⌧0 follows a strategy str if ⌧i = str(⌧i-1↪ ↵i) for every i ≥ 1.

Theorem1. Assume aKBKand an assertion q. ThenK6♣= q iff there is a core interpretations Ic for K such that:

For a finite run w, we let tail(w) = type(a↪ I) if w = a, and tail(w) = ⌧` if w = a ▷ ▷ ▷ ↵`⌧` with ` ≥ 1. The strategy str is called non-losing on I if for every finite run w that follows str, tail(w) 2 LC(T ↪⌃↪ I) and str(tail(w)↪Av 9r▷A0 ) is defined for every Av9r▷A0 2 T with A 2 tail(w).

1. Ic 6♣= q, and
2. there is a non-losing strategy for Bob on Ic.

Proof. (Sketch.) We focus on showing that there is a nonlosing strategy str for Bob on Ic iff there exists an extension J of Ic s.t. J ♣= K. The claim follows from this, and the easy claim that extensions preserve non-entailment of q.

For the "(" direction, we assume an arbitrary extension J of Ic that models K, and let T be a the set of all the types realized in J . For each ⌧ 2 T and each Av 9r▷A0 2 T with A 2 ⌧, let str(⌧↪A v 9r▷A0 ) = ⌧ 0 for an arbitrarily chosen ⌧ 0 2 T that satisfies (C1) and (C2), which exists because J is a model. This str is a non-losing strategy for Bob on Ic.

We denote by frn(Ic↪ str) the set of all finite runs a↵1⌧1 · · · that follow str where each ⌧i, i ≥ 1, are not fixed types, and by fxr(Ic↪ str) the set of all finite runs a↵1⌧1 · · · ↵`⌧` that follow str, where ⌧` is a fixed type, and each ⌧i, 1  i < `, is not a fixed type. The domain of J is:

For the ")" direction, from an arbitrary non-losing str for Ic, we build J as follows. We call a type ⌧ fixed if it contains a nominal ¶a♦, some A 2 ⌃, or some A with Av9r▷A0 2 T , r v s 2 T and s(-) 2 ⌃; note that fixed types cannot be realized by domain objects outside the core. For each fixed ⌧ that is realized in Ic, we let a⌧ denote a fixed, arbitrary individual realizing ⌧ (in particular, a⌧ = b if ¶b♦ 2 ⌧).

and for each a 2 NI, each A 2 NC, and each p 2 NR we let:

where ↵i = A v 9ri▷A0 2 T and ¶w↪ w↵i⌧i↪ a⌧i ♦ ✓ ∆J .

Note that the interpretation is well defined, since w↵i⌧i 2 fxr(Ic↪ str) implies that ⌧i is a fixed type in LC(T ↪⌃↪ Ic), which guarantees that ⌧i is realized in Ic and that a⌧i exists. One can show that J ♣= K. Roughly, J ♣=⌃ A is a direct consequence of the definition of Ic and the fact that J is its

Algorithm 1: Mark

input : TBox T , set ⌃ ✓ NC [NR, interpretation I output: Set of (possibly marked) types

(MN1) Mark each ⌧ 2 N that violates some inclusion of the form (N1) in T

(M⌃) Mark each ⌧ 2 N such that ⌧ is not realized in I and one of the following holds:

• (i) ⌧ \⌃6= ;, or

(MO) Mark each ⌧ 2N with ¶a♦ 2 ⌧ and ⌧ 6= type(a↪ I) repeat

(M9) Mark each ⌧ 2 N such that A v 9r▷A0 2 T , A 2 ⌧ , and for each ⌧ 0 2 N, at least one the following holds:

• (C0) ⌧ 0 is marked,
• (C10 ) A0 ◁2 ⌧ 0 , or
• (i) r v s 2 T and A1 2 ⌧ and A2 ◁2 ⌧ 0 , or
• (C20 ) there exists A1 v8s▷A2 2 T with
• (ii) r- v s 2 T and A1 2 ⌧ 0 and A2 ◁2 ⌧

until no new type is marked return N

extension. We can similarly argue that J satisfies the inclusions in T for the individuals. For the fresh objects, it follows from the fact that they have as children in J the types given by the strategy, which are suitable successors.

To decide whether Bob has a non-losing strategy on a given core we use the type elimination procedure Mark in Algorithm 1, which marks (or, eliminates) all types from which Sam has a strategy to defeat Bob. It takes as input the TBox T , the set ⌃ ✓ NC [ NR, and an interpretation I which intuitively is the core being checked. The algorithm starts by building the set N of all possible types over T , and then it marks types that are bad choices for Bob (since they give Sam a way to defeat him). In steps (MN1), (M⌃) and (MO) the algorithm respectively marks in N all types that violate the condition (LCN1), (LC⌃) or (LCO); Sam wins already in the first round on these types. Then, in the loop, (M9) exhaustively marks types ⌧ that allow Sam to pick an inclusion A v 9r▷A0 for which Bob cannot reply with any ⌧ 0 .

The formal relationship between the game and the marking algorithm is established in the following theorem.

Theorem 2. Let Ic be a core interpretation. Then Bob has a non-losing strategy on Ic iff none of the types realized in Ic is marked by Mark(T ↪ ⌃↪ Ic).

Proof. (Sketch.) For the ")" direction, we can show (by induction in the number of iterations of Mark(T ↪⌃↪ Ic)) that if a type is marked, then it cannot occur in a non-losing str for Bob. For the "(" direction, a non-losing str for Ic is obtained by taking all unmarked ⌧ 2 N, and for each of them, and each Av 9r▷A0 2 T with A 2 ⌧, setting str(⌧↪Av 9r▷A0 ) = ⌧ 0 for an arbitrary unmarked ⌧ 0 that satisfies (C1) and (C2).

4 Rewriting into Nonmonotonic Disjunctive Datalog

Assume an instance query (T ↪⌃↪ q). We build next a polynomially sized program P such that the queries (T ↪ ⌃↪ q) and (P↪ q) have the same certain answers for all ABoxes over the signature of T . Roughly, the program P consists of 3 major components described as follows:

• (a) rules to non-deterministically generate a core interpretation Ic for the KB (T ↪ ⌃↪ A), where A is an input ABox;
• (b) rules that implement the type elimination algorithm presented in the previous section;
• (c) rules that glue (a) and (b) together, ensuring that all types that occur in Ic are not marked by the marking procedure.

We remark that the construction of P is independent from any particular ABox.

• (I) Collecting the individuals We first add rules to collect in the unary predicate ind all the individuals that occur in T or the input ABox. For each A 2 NC(T ), r 2 NR(T ), and nominal ¶a♦ that occurs in T we have:

• (II) Generating core interpretations For each A 2 NC(T )∩⌃ (resp., r 2 NR(T )∩⌃) we will use a fresh concept name A (resp., role name r). We add the following rules to P :

To ensure (c3) in Definition 1, for each A v 8r▷A0 2 T we add one of the following:

To ensure (c4), for each role inclusion r v s 2 T we add one of the following:

In principle, a constraint A(x)↪ r(x↪ y)↪ not A0 (y) could be for all concept names, not only closed ones. We make the distinction here and later in order to eventually obtain a positive program in case ⌃ = ;.

To ensure (c5), for each inclusion A v 9r▷A0 2 T with r v s 2 T and s(-) 2 ⌃, add the following rules Here RA0 is a fresh predicate symbol.

Intuitively, the stable models of the above rules generate the different core interpretations Ic of the KB K = (T ↪ ⌃↪ A) for any given A. We next implement the algorithm Mark from Section 3. To obtain a polynomially sized program, we need to use non-ground rules whose number of variables depends on the number of different concept names and nominals in T . Assume an arbitrary enumeration B1↪ ▷ ▷ ▷ ↪Bk of N+C (T ), i.e. of the concept names and nominals that occur in T . Assume also a pair 0↪ 1 of special individuals. Intuitively, we will use a k-ary relation Type = ¶0↪ 1♦k to store the set of all types over T . Naturally, a k-tuple (b1↪ ▷ ▷ ▷ ↪ bk) 2 Type encodes the type ⌧ = ¶Bi ♣ bi = 1↪ 1  i  k♦ [ ¶>♦. We are most interested in computing a k-ary relation Marked ✓ ¶0↪ 1♦k that contains precisely the types marked by the Mark algorithm. We next define the rules to compute Type and Marked, and other relevant relations.

(III) A linear order over types We use k-ary relation symbols first and last, and add the facts first(0↪ ▷ ▷ ▷ ↪ 0) and last(1↪ ▷ ▷ ▷ ↪ 1) . We also use a 2k-ary relation next that will store a lexicographic ordering over ¶0↪ 1♦k with (0↪ ▷ ▷ ▷ ↪ 0) and (1↪ ▷ ▷ ▷ ↪ 1) the first and the last element, respectively. That is, given ~u↪ ~v 2 ¶0↪ 1♦k , the fact next(~u↪ ~v) is true if ~v follows ~u in a lexicographic ordering. The rules to populate next are standard (see, e.g., Theorem 4.5 in [Dantsin et al., 2001]).

We can now collect in the k-ary relation Type all types over T (thus computing the set N of theMark algorithm):

(IV) Implementing Step (MN1) First, we add the auxiliary facts F(0) and T(1) to P. For a k-tuple of variables ~x, we let B 2 ~x denote the atom T(xj), where j is the index of B in the enumeration of N+C (T ). Similarly, we let B 62 ~x denote the atom F(xj), where j is the index of B in the enumeration.

Then the step (MN1), which marks types violating inclusions of type (N1), is implemented using the following rule for every inclusion B1 u · · · u Bn v Bn+1 t · · · t Bk 2 T :

• (V) Collecting realized types We employ (i+1)-ary ("has type") relations hasTi for all 0  i  k. We add the rule hasT0 (x) ind(x), and the following rules for all 1ik:

Intuitively, hasTk stores the type of individuals in a generated core interpretation for the KB. I.e. the fact hasTk (c↪~v) says that the individual c has the type that is encoded in the bit vector ~v. We can now project away the individuals and store in the relation RealizedType the set of realized types:

(VI) Implementing Step (M⌃) In this step, we mark all non-realized types that contain a closed concept name, or enforce an s-neighbor with s(-) 2 ⌃. In particular, for (i) every A 2 NC(T )\⌃, and (ii) every inclusion Av9r▷A0 2 T with r v s 2 T and s(-) 2 ⌃, we add the rule

(VII) Implementing Step (MO) This step marks every nominal-containing type that is not realized in the core interpretation. We implement it by adding the following rules for all B 2 N+C and all nominals ¶a♦ that occur in T :

(VIII) Implementing Step (M9) The following rules are added for all inclusions ↵ = Av 9r▷A0 2 T . Recall that we need to mark a type ⌧ if A 2 ⌧, and for each type ⌧ 0 2 N at least one of (C0), (C10 ) or (C20 ) holds. First, for each such inclusion ↵, we use an auxiliary 2k-ary relation MarkedOne↵ to collect all such types ⌧ 0 .

• For collecting each ⌧ 0 that satisfies (C0), we add:

• For the condition (C10 ), we add the rule:

• The rules for (C20 ) are as follows.
• For all A1 v 8s▷A2 2 T with r v s 2 T , we add:

• For all A1 v 8s▷A2 2 T with r- v s 2 T , we also add:

Intuitively, we want to infer Marked(~t) if A is set to true in ~t and MarkedOne↵(~t↪~v) is true for all types (bit vectors) ~v. To achieve this, we rely on another auxiliary 2k-ary relation MarkedUntil↵ for each inclusion ↵:

Intuitively, with the above rules we traverse all types checking the conditions (C0), (C10 ), (C20 ) described in (M9). If we manage to reach the last type, and if A 2 ~x, then we know the condition is satisfied and mark the type:

(IX) Forbiddingmarked types in the core We need to forbid each individual in the generated core interpretation from having a type from Marked. For all 0  i  k, we take a fresh (i + 1)-ary relation symbol Proji . We first add:

We will now project away bits from the Proji relations by looking at the actual types of individuals. For all 1  i  k we have the following rules:

Intuitively, Proji-1 (a↪ b1↪ ▷ ▷ ▷ ↪ bi-1) says the partial type given by the bit values b1↪ ▷ ▷ ▷ ↪ bi-1 can be extended to a marked type by choosing additional concepts according to the actual type of the individual a. Thus the fact Proj0 (a) represents the situation where a has a marked type. Such situations are ruled out by adding the constraint Proj0 (x).

This concludes the rewriting of the instance query (T ↪⌃↪ q) into the program P. In case ⌃ = ;, our rewriting does not use not in rule bodies. If nominals are not present in T , we also don't use the predicate 6=. This construction together with Theorems 1 and 2 yields our main result:

Theorem 3. For an instance query (T ↪⌃↪ q), where T is an ALCHIO TBox, we can build in polynomial time a query (P↪ q), where P may use disjunction and negation, such that:

• (i) The certain answers to (T ↪ ⌃↪ q) and (P↪ q) coincide for any given ABox A over the signature of T .
• (ii) If ⌃ = ;, then P is a positive program.
• (iii) If ⌃ = ; and T is anALCHI TBox, thenP is a positive program with no occurrences of the 6= predicate.

The above encoding employs disjunction, and possibly negation as failure. Entailment of ground atoms already in positive disjunctive programs is coNEXPTIME-complete [Eiter et al., 1997], which does not match the EXPTIMEcompleteness of satisfiability of ALCHIO KBs with (or without) closed predicates. However, we employ disjunction and negation in a limited way, and thus our programs fall into a class of programs that can be evaluated in (deterministic) exponential time. In particular, the above program P can be partitioned ("stratified") into programs P1↪ P2↪ P3 as follows:

• P1 consists of all rules in (I) and (II), except the constraints. P1 is a positive disjunctive program with at most two variables in each rule.
• P2 consists of the constraints in (II), and the rules in (V). Intuitively, the disjunction-free P2 ensures that P1 generates a proper core interpretation, and computes the types realized in it.
• P3 consists of the remaining rules, and is disjunction-free.

Note that P2 and P3 do not define any relations used in P1, i.e. none of the relation symbols of P1 occurs in the head of a rule in P2[P3. The program P2 only depends on P1, i.e. none of relation symbols in P2 occurs in the head of a rule in P3. The negative atoms of P2 only involve relations that are fully defined by P1, i.e. such relation do not appear in the head of rule in P2. Similarly, the negative atoms of P3 only involve relations that are fully defined by P1 [P2. Assume a set F of facts over the signature of P1. Due to the above properties, the successful runs of the following non-deterministic procedure generate the set of all stable models of P [ F :

• (S1) Compute a minimal model I1 of P1 [ F .
• (S2) Compute the least model I2 of I1 [ P I1 2 . If I2 does not exist due to a constraint violation, then return failure.
• (S3) Compute the least model I3 of I2 [ P I2 2 . Again, if I3 does not exist, then return failure. Otherwise, output I3.

Since P1 has at most two-variables in every rule, each minimal model I1 of P1 [ F is of polynomial size in the size of P1 [ F, and the set of all such models can be traversed in polynomial space. For a given I1, performing steps (S2) and (S3) is feasible in (deterministic) exponential time, because P I1 2 and the subsequent P I2 2 are ground disjunction-free positive programs of exponential size. It follows that computing the certain answers to (P↪ q) for any given ABox A over the signature of T requires single exponential time.

We remark that if there are no closed predicates, i.e. in case ⌃ = ;, the resulting program has an even simpler structure. It contains all rules of P that do not have not in rule bodies, and it can be partitioned into two programs:

• a disjunctive programP1 with at most two variables in each rule, which can include all positive rules in (I) and (II);
• a disjunction-free P2 that does not define any relations in P1, which consists all the remaining rules.

Analogously as above, we can evaluate P over a given set F of facts, by traversing the minimal models I1 of P1 [ F , and for each I1, verifying in (deterministic) exponential time if it can be extended to a model of P2. More details about this case, but without nominals, i.e. for the DL ALCHI, can be found in [Ahmetaj et al., 2016].

5 Discussion

We note that 6=-free positive programs are not expressive enough to capture instance queries (T ↪ ;↪ q) when T has nominals. This follows from the following observation. For any positive 6=-free program P and a set of facts F , if P [ F has a model, then also P [ F 0 has a model, were F 0 is obtained from F by renaming its constants with fresh ones that don't occur in P [F . However, this property cannot be recast to ALCHIO. Take the TBox T = ¶Av ¶a♦♦ and observe that T is consistent w.r.t. the ABox A1 = ¶A(a)♦, but is inconsistent w.r.t. the ABox A2 = ¶A(b)♦.

We have presented our results for ALCHIO, but they also apply to SHIO, using standard techniques to eliminate transitivity axioms (see, e.g., [Hustadt et al., 2007]). Moreover, the results can be easily generalized, e.g., to DL-safe rules of [Motik et al., 2005], or the quantifier-free CQs like in [Lutz et al., 2015]. These queries are syntactically restricted to ensure that the relevant variable assignments only map into individuals of the input ABox. Under common assumptions in complexity theory, our translation cannot be generalized to CQs, while remaining polynomial. This is because cautious inference from a disjunctive program with negation is in coNEXPTIME NP , but entailment of (Boolean) CQs is 2EXPTIME-hard already for the DL ALCI [Lutz, 2007].

Acknowledgments

In memory of Helmut Veith (1971-2016).

This work was supported by the Austrian Science Fund (FWF) projects P25207, T515 and W1255.